NO 1.756 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be disproven:



↳ HASKELL
  ↳ BR

mainModule Main
  ((readFile :: [Char]  ->  IO [Char]) :: [Char]  ->  IO [Char])

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Main
  ((readFile :: [Char]  ->  IO [Char]) :: [Char]  ->  IO [Char])

module Main where
  import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow

mainModule Main
  (readFile :: [Char]  ->  IO [Char])

module Main where
  import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ NonTerminationProof
          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_readFile(vx3) → new_readFile(vx3)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_readFile(vx3) → new_readFile(vx3)

The TRS R consists of the following rules:none


s = new_readFile(vx3) evaluates to t =new_readFile(vx3)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_readFile(vx3) to new_readFile(vx3).




Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow
            ↳ QDP
              ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

new_readFile(vx3, []) → new_readFile(vx3, [])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_readFile(vx3, []) → new_readFile(vx3, [])

The TRS R consists of the following rules:none


s = new_readFile(vx3, []) evaluates to t =new_readFile(vx3, [])

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_readFile(vx3, []) to new_readFile(vx3, []).